//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
//	* Mateusz Ujma <mateusz.ujma@cs.ox.ac.uk> (University of Oxford)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM is free software; you can redistribute it and/or modify
//	it under the terms of the GNU General Public License as published by
//	the Free Software Foundation; either version 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM is distributed in the hope that it will be useful,
//	but WITHOUT ANY WARRANTY; without even the implied warranty of
//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
//	GNU General Public License for more details.
//	
//	You should have received a copy of the GNU General Public License
//	along with PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package com.prism.e4.rcp.explicit;

import java.io.File;
import java.util.ArrayList;
import java.util.BitSet;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;

import com.prism.e4.rcp.parser.State;
import com.prism.e4.rcp.parser.Values;
import com.prism.e4.rcp.parser.VarList;
import com.prism.e4.rcp.prism.ModelType;
import com.prism.e4.rcp.prism.PrismException;
import com.prism.e4.rcp.prism.PrismLog;

/*
 * Class for creating a sub-model of any NondetModel, please note the translate* methods
 * used to translate between state ids for model and sub-model. Created sub-model will have new 
 * state numbering from 0 to number of states in the sub model.
 * 
 */

public class SubNondetModel implements NondetModel {

	private NondetModel model = null;
	private BitSet states = null;
	private Map<Integer, BitSet> actions = null;
	private BitSet initialStates = null;
	private List<State> statesList = null;
	private Map<Integer, Integer> stateLookupTable = new HashMap<Integer, Integer>();
	private Map<Integer, Map<Integer, Integer>> actionLookupTable = new HashMap<Integer, Map<Integer, Integer>>();
	private Map<Integer, Integer> inverseStateLookupTable = new HashMap<Integer, Integer>();

	private int numTransitions = 0;
	private int maxNumChoices = 0;
	private int numChoices = 0;

	public SubNondetModel(NondetModel model, BitSet states,
			Map<Integer, BitSet> actions, BitSet initialStates) {
		this.model = model;
		this.states = states;
		this.actions = actions;
		this.initialStates = initialStates;

		generateStatistics();
		generateLookupTable(states, actions);
	}

	@Override
	public ModelType getModelType() {
		return model.getModelType();
	}

	@Override
	public int getNumStates() {
		return states.cardinality();
	}

	@Override
	public int getNumInitialStates() {
		return initialStates.cardinality();
	}

	@Override
	public Iterable<Integer> getInitialStates() {
		List<Integer> is = new ArrayList<Integer>();
		for (int i = initialStates.nextSetBit(0); i >= 0; i = initialStates
				.nextSetBit(i + 1)) {
			is.add(translateState(i));
		}

		return is;
	}

	@Override
	public int getFirstInitialState() {
		return translateState(initialStates.nextSetBit(0));
	}

	@Override
	public boolean isInitialState(int i) {
		return initialStates.get(translateState(i));
	}

	@Override
	public int getNumDeadlockStates() {
		throw new UnsupportedOperationException();
	}

	@Override
	public Iterable<Integer> getDeadlockStates() {
		throw new UnsupportedOperationException();
	}

	@Override
	public StateValues getDeadlockStatesList() {
		throw new UnsupportedOperationException();
	}

	@Override
	public int getFirstDeadlockState() {
		throw new UnsupportedOperationException();
	}

	@Override
	public boolean isDeadlockState(int i) {
		throw new UnsupportedOperationException();
	}

	@Override
	public List<State> getStatesList() {
		// We use lazy generation because in many cases the state list is not
		// needed
		if (statesList == null) {
			statesList = generateSubStateList(states);
		}
		return statesList;
	}

	private List<State> generateSubStateList(BitSet states) {
		List<State> statesList = new ArrayList<State>();
		for (int i = 0; i < model.getNumStates(); i++) {
			if (states.get(i)) {
				statesList.add(model.getStatesList().get(i));
			}
		}
		return statesList;
	}

	@Override
	public Values getConstantValues() {
		throw new UnsupportedOperationException();
	}

	@Override
	public int getNumTransitions() {
		return numTransitions;
	}

	@Override
	public Iterator<Integer> getSuccessorsIterator(int s) {
		s = translateState(s);

		List<Integer> succ = new ArrayList<Integer>();
		for (int i = 0; i < model.getNumChoices(s); i++) {
			if (actions.get(s).get(i)) {
				Iterator<Entry<Integer, Double>> it = model
						.getTransitionsIterator(s, i);
				while (it.hasNext()) {
					int succc = it.next().getKey();
					succ.add(inverseTranslateState(succc));
				}
			}
		}
		return succ.iterator();
	}

	@Override
	public boolean isSuccessor(int s1, int s2) {
		s1 = translateState(s1);
		s2 = translateState(s2);
		return model.isSuccessor(s1, s2);
	}

	@Override
	public boolean allSuccessorsInSet(int s, BitSet set) {
		throw new UnsupportedOperationException();
	}

	@Override
	public boolean someSuccessorsInSet(int s, BitSet set) {
		throw new UnsupportedOperationException();
	}

	@Override
	public void findDeadlocks(boolean fix) throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public void checkForDeadlocks() throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public void checkForDeadlocks(BitSet except) throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public void exportToPrismExplicit(String baseFilename)
			throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public void exportToPrismExplicitTra(String filename) throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public void exportToPrismExplicitTra(File file) throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public void exportToPrismExplicitTra(PrismLog log) throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public void exportToDotFile(String filename) throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public void exportToDotFile(String filename, BitSet mark)
			throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public void exportToPrismLanguage(String filename) throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public void exportStates(int exportType, VarList varList, PrismLog log)
			throws PrismException {
		throw new UnsupportedOperationException();
	}

	@Override
	public String infoString() {
		throw new UnsupportedOperationException();
	}

	@Override
	public String infoStringTable() {
		throw new UnsupportedOperationException();
	}

	@Override
	public int getNumChoices(int s) {
		s = translateState(s);
		return actions.get(s).cardinality();
	}

	@Override
	public int getMaxNumChoices() {
		return maxNumChoices;
	}

	@Override
	public int getNumChoices() {
		return numChoices;
	}

	@Override
	public Object getAction(int s, int i) {
		s = translateState(s);
		i = translateAction(s, i);

		return model.getAction(s, i);
	}

	@Override
	public boolean allSuccessorsInSet(int s, int i, BitSet set) {
		s = translateState(s);
		i = translateAction(s, i);
		set = translateSet(set);

		return model.allSuccessorsInSet(s, i, set);
	}

	@Override
	public boolean someSuccessorsInSet(int s, int i, BitSet set) {
		s = translateState(s);
		i = translateAction(s, i);
		set = translateSet(set);

		return model.someSuccessorsInSet(s, i, set);
	}

	private BitSet translateSet(BitSet set) {
		BitSet translatedBitSet = new BitSet();
		for (int i = set.nextSetBit(0); i >= 0; i = set.nextSetBit(i + 1)) {
			translatedBitSet.set(translateState(i));
		}
		return translatedBitSet;
	}

	private void generateStatistics() {
		for (int i = 0; i < model.getNumStates(); i++) {
			if (states.get(i)) {
				numTransitions += getTransitions(i);
				numChoices += actions.get(i).cardinality();
				maxNumChoices = Math.max(maxNumChoices, model.getNumChoices(i));
			}
		}
	}

	private int getTransitions(int state) {
		int transitions = 0;
		for (int i = 0; i < model.getNumChoices(state); i++) {
			Iterator<Entry<Integer, Double>> it = model.getTransitionsIterator(
					state, i);
			while (it.hasNext()) {
				it.next();
				transitions += 1;
			}
		}
		return transitions;
	}

	@Override
	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s, int i) {
		s = translateState(s);
		i = translateAction(s, i);

		Map<Integer, Double> distrs = new HashMap<Integer, Double>();
		Iterator<Entry<Integer, Double>> it = model
				.getTransitionsIterator(s, i);
		while (it.hasNext()) {
			Entry<Integer, Double> e = it.next();
			int succ = inverseTranslateState(e.getKey());
			distrs.put(succ, e.getValue());
		}
		return distrs.entrySet().iterator();
	}

	private void generateLookupTable(BitSet states, Map<Integer, BitSet> actions) {
		for (int i = 0; i < model.getNumStates(); i++) {
			if (states.get(i)) {
				inverseStateLookupTable.put(i, stateLookupTable.size());
				stateLookupTable.put(stateLookupTable.size(), i);
				Map<Integer, Integer> r = new HashMap<Integer, Integer>();
				for (int j = 0; j < model.getNumChoices(i); j++) {
					if (actions.get(i).get(j)) {
						r.put(r.size(), j);
					}
				}
				actionLookupTable.put(actionLookupTable.size(), r);
			}
		}
	}

	public int translateState(int s) {
		return stateLookupTable.get(s);
	}

	private int inverseTranslateState(int s) {
		return inverseStateLookupTable.get(s);
	}

	public int translateAction(int s, int i) {
		return actionLookupTable.get(s).get(i);
	}
}

// ------------------------------------------------------------------------------